i,x:Id, T:Type, L:(Knd List).
normal-type{i:l}(T)  R-realizes{i:l}(Rframe(i; T; x; L); es.frame-p(es; i; T; x; L)) 

latex

Definitions	t  T, R-Feasible{i:l}(R), P  Q, R-realizes{i:l}(R; es.P(es)), P  Q, x:A. B(x), R-consistent(R; es), prop{i:l}
Lemmas	Id wf, Knd wf, normal-type wf, event system wf, Rframe wf, R-consistent wf